部署在區塊鏈上的智慧合約可能會操縱高價值資產。作為一種使用嚴格的數學方法來描述電腦系統的行為和推理正確性的技術，形式化驗證已被用於區塊鏈中以防止智能合約中的錯誤。 Move 驗證器 是一種不斷發展的形式驗證工具，用於用 Move 語言編寫的智能合約。使用者可以使用行動規範語言（MSL）指定智慧合約的功能屬性 ，然後使用證明者自動靜態檢查它們。為了說明如何使用驗證器，我們在 BasicCoin.move 中加入了以下程式碼片段：

    spec balance_of {
        pragma aborts_if_is_strict;
    }

通俗地說，區塊裡 spec balance_of {...}包含方法的屬性規範 balance_of。

BasicCoin 讓我們先在目錄中使用以下命令執行證明程式：

move prove

輸出如下錯誤訊息：

error: abort not covered by any of the `aborts_if` clauses
   ┌─ ./sources/BasicCoin.move:38:5
   │
35 │           borrow_global<Balance<CoinType>>(owner).coin.value
   │           ------------- abort happened here with execution failure
   ·
38 │ ╭     spec balance_of {
39 │ │         pragma aborts_if_is_strict;
40 │ │     }
   │ ╰─────^
   │
   =     at ./sources/BasicCoin.move:34: balance_of
   =         owner = 0x29
   =     at ./sources/BasicCoin.move:35: balance_of
   =         ABORTED

Error: exiting with verification errors 

驗證器基本上告訴我們，我們需要明確指定函數將中止的條件，這是由於在不擁有資源時balance_of呼叫函數而導致的。為了刪除這個錯誤訊息，我們新增一個條件如下：

borrow_global 當 owner 不再擁有資源 Balance 時就放棄 aborts_if 來消除error.

    spec balance_of {
        pragma aborts_if_is_strict;
        aborts_if !exists<Balance<CoinType>>(owner);
    }

新增此條件後，嘗試再次執行該prove命令以確認不存在驗證錯誤：

move prove